proposition: Lemma hnf_proofs_sound : forall e t T, typ e t T -> normal t -> hnf_proofs e t.
proof: Proof. simple induction 1; simpl in |- *; intros; auto. apply is_atom_app. elim prod_inhabitants with (1 := H2) (a := V) (b := Ur); intros; auto with coc. inversion_clear H5. inversion_clear H6. rewrite H5 in H4. elim H4 with (subst v x0); auto with coc. red in |- *; red in |- *; intros. elim H4 with (App u0 v); auto with coc. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia