proposition: Lemma atom_inhabitants : forall e t u u', typ e t u -> conv u u' -> is_atom e u' -> hnf_proofs e t -> is_atom e t.
proof: Proof. simple induction 1; simpl in |- *; intros; auto. elim conv_sort_atom with (1 := H2) (2 := H1). elim conv_sort_atom with (1 := H2) (2 := H1). split with v. inversion_clear H1. elim H6; simpl in |- *; auto with arith. split with (nil (A:=term)); auto. elim conv_prod_atom with (1 := H7) (2 := H6). elim conv_sort_atom with (1 := H5) (2 := H4). apply H1; auto. apply trans_conv_conv with V; auto with coc. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia