Skip to content
Snippets Groups Projects
Commit 00cab5cd authored by Michael Sammler's avatar Michael Sammler
Browse files

comment

parent d09be351
No related branches found
No related tags found
No related merge requests found
Pipeline #43094 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/module.v
+ 1
− 1
View file @ 00cab5cd
...@@ -976,7 +976,7 @@ Proof. ...@@ -976,7 +976,7 @@ Proof.
- move => ???? /Hinvnonempty [??]. eexists _. split => //. by apply: TraceEnd. - move => ???? /Hinvnonempty [??]. eexists _. split => //. by apply: TraceEnd.
- move => σi1 σi2 σi3 κ κs Hstep Hsteps IH σs1 Hinv. - move => σi1 σi2 σi3 κ κs Hstep Hsteps IH σs1 Hinv.
have := Hinvstep _ _ _ _ Hinv Hstep. have := Hinvstep _ _ _ _ Hinv Hstep.
(* TODO: continue here *) (* TODO: continue here. The lemma statement is probably wrong *)
have [σs2 [Hinv2 Hsub]]:= Hinvstep _ _ _ _ Hinv Hstep. have [σs2 [Hinv2 Hsub]]:= Hinvstep _ _ _ _ Hinv Hstep.
have [σs3 [σs4 [Hin ?]]]:= IH _ Hinv2. have [σs3 [σs4 [Hin ?]]]:= IH _ Hinv2.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment