proposition: Lemma inv_Ered_Abs : forall T U x : term, Ered (Abs T U) x -> exists T' : term, (exists U' : term, x = Abs T' U').
proof: Proof. simple induction 1. split with T; split with U; trivial. intros P N H0 (T', (U', H1)) H2. rewrite H1 in H2. inversion H2. split with (Srt prop); split with U'; trivial. split with M'; split with U'; trivial. split with T'; split with M'; trivial. Qed.
imports: Termes Conv