proposition: Lemma Ered_Enormal : forall u v : term, Ered u v -> Enormal u -> u = v.
proof: Proof. simple induction 1; auto with ecoc coc core arith sets; intros. absurd (Ered1 u N); auto with ecoc coc core arith sets. absurd (Ered1 P N); auto with ecoc coc core arith sets. elim (H1 H3). unfold not in |- *; intro; apply (H3 N); auto with ecoc coc core arith sets. Qed.
imports: Termes Conv