proposition: Lemma conv_prod_atom : forall a b e u, is_atom e u -> ~ conv (Prod a b) u.
proof: Proof. red in |- *; intros. elim church_rosser with (1 := H0); intros. apply red_prod_prod with (1 := H1); intros. rewrite H3 in H2. specialize atom_reduction with (1 := H2) (2 := H). apply prod_not_atom. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia