Commit ae9857fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak.

parent 4d86571d
......@@ -132,24 +132,9 @@ Section stype_ofe.
| _, _ => False
end.
Proof.
uPred.unseal; constructor=> n x ?.
split.
- intros Heq.
destruct st1, st2.
+ constructor.
+ inversion Heq.
+ inversion Heq.
+ inversion Heq; subst.
repeat split; eauto.
- intros Heq.
destruct st1, st2.
+ constructor.
+ inversion Heq.
+ inversion Heq.
+ inversion Heq; subst.
rewrite H.
constructor.
apply H0. apply Heq.
uPred.unseal; constructor=> n x ?. split; first by destruct 1.
destruct st1, st2=> //=; [constructor|].
by intros [[= ->] [??]]; constructor.
Qed.
End stype_ofe.
Arguments stypeC : clear implicits.
......
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