proposition: Lemma Econv_abs : forall a b T : term, Econv a b -> Econv (Abs T a) (Abs T b).
proof: Proof. intros. elim H; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with (Abs T P); auto with ecoc coc core arith sets. apply Etrans_conv_exp with (Abs T P); auto with ecoc coc core arith sets. Qed.
imports: Termes Conv