The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

I just have to suggest this alternative way to prove it.


Ltac mark H := let T := type of H in change (id T) in H.
Ltac unmark := unfold id in *.

Fact totalf {a a'} (F : f a a') : a = a'
with totalg {l l'} (G : g l l') : l = l'.
Proof.
  
  Ltac information f f' := repeat match goal with F : f _ _ |- _ => pose (f'
_ _ F); mark F end.
  
  intros; destruct F; information f totalf; information g totalg;
congruence.
  intros; destruct G; information f totalf; information g totalg;
congruence.

Qed.


-- 
View this message in context: 
http://old.nabble.com/Properties-on-mutual-definitions-tp26711958p26716597.html
Sent from the Coq mailing list archive at Nabble.com.