Commit 4f37b123 authored by charguer's avatar charguer
Browse files

dfs_proof

parent a26fd78b
......@@ -92,7 +92,7 @@ Lemma reachables_monotone : forall G E1 E2 F1 F2,
F2 \c F1 ->
reachables G E2 F2.
Proof using.
skip.
introv R HE HF. rewrite incl_in_eq in HE,HF. skip.
Qed.
Lemma reachables_trans : forall G E1 E2 E3,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment