The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

muad wrote:
> 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.
>   

The theorem doesn't seem to need so complex a proof.

Scheme f_mut := Minimality for f Sort Prop
with g_mut := Minimality for g Sort Prop.
Combined Scheme fg_mut from f_mut, g_mut.

Fact total :
(forall a a', f a a' -> a = a')
/\ (forall l l', g l l' -> l = l').
apply fg_mut; intros; subst; reflexivity.
Qed.