proposition: Lemma inv_Epar_red_abs : forall (P : Prop) (T U x : term), Epar_red1 (Abs T U) x -> (forall T' U' : term, x = Abs T' U' -> Epar_red1 U U' -> P) -> P.
proof: Proof. do 5 intro. inversion_clear H; intros. apply H with (Srt prop) M'; auto with ecoc. apply H with T' M'; auto with ecoc. Qed.
imports: Termes Conv