proposition: Lemma sym_Econv : forall M N : term, Econv M N -> Econv N M.
proof: Proof. simple induction 1; auto with ecoc coc core arith sets. simple induction 2; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with P0; auto with ecoc coc core arith sets. apply Etrans_conv_exp with P0; auto with ecoc coc core arith sets. simple induction 2; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with P0; auto with ecoc coc core arith sets. apply Etrans_conv_exp with P0; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv