proposition: Lemma inv_par_red_abs : forall (P : Prop) T (U x : term), par_red1 (Abs T U) x -> (forall T' (U' : term), x = Abs T' U' -> par_red1 U U' -> P) -> P.
proof: Proof. do 5 intro. inversion_clear H; intros. apply H with T' M'; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations