proposition: Lemma conv_sort : forall s1 s2, conv (Srt s1) (Srt s2) -> s1 = s2.
proof: Proof. intros. cut (Srt s1 = Srt s2); intros. injection H0; auto with coc core arith sets. apply nf_uniqueness; auto with coc core arith sets. red in |- *; red in |- *; intros. inversion_clear H0. red in |- *; red in |- *; intros. inversion_clear H0. Qed.
imports: Termes