- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
Lemma mint_head_eq CR1 CR2 (te : TE) l m r (t t' : list TE) :
MInt CR1 (l, m, r) (te :: t) ->
MInt CR2 (l, m, r) t' ->
exists t'', t' = te :: t''.
Proof.
intros H1 H2.
inversion_ H1; inversion_ H2; (* generates 25 goals *)
match goal with
|- (exists _, te :: ?T = te :: _) => now exists T
end.
Qed.
Follow us!