proposition: Lemma conv_sort_atom : forall (s : sort) e u, is_atom e u -> ~ conv (Srt s) u.
proof: Proof. red in |- *; intros. elim church_rosser with (1 := H0); intros. rewrite <- red_normal with (1 := H1) in H2. specialize atom_reduction with (1 := H2) (2 := H). apply sort_not_atom. red in |- *; red in |- *; intros. inversion H3. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia