proposition: Lemma nf_uniqueness : forall u v, conv u v -> normal u -> normal v -> u = v.
proof: Proof. intros. elim church_rosser with u v; intros; auto with coc core arith sets. rewrite (red_normal u x); auto with coc core arith sets. elim red_normal with v x; auto with coc core arith sets. Qed.
imports: Termes