proposition: Lemma prod_inhabitants : forall e t u, typ e t u -> forall a b, conv u (Prod a b) -> normal t -> is_atom e t \/ (exists a' : _, (exists m : _, t = Abs a' m)).
proof: Proof. simple induction 1; intros; eauto. elim conv_sort_prod with (1 := H1). elim conv_sort_prod with (1 := H1). left. exists v. inversion_clear H1. elim H5; intros; simpl in |- *; auto with arith. exists (nil (A:=term)); simpl in |- *; auto. left. apply is_atom_app. elim H3 with V Ur; intros; auto with coc. inversion_clear H6. inversion_clear H7. rewrite H6 in H5. elim H5 with (subst v x0); auto with coc. red in |- *; red in |- *; intros. elim H5 with (App u1 v); auto with coc. elim conv_sort_prod with (1 := H4). apply H1 with a b; auto. apply trans_conv_conv with V; auto. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia