proposition: Lemma coc_consistency_nf : forall t, normal t -> ~ typ nil t absurd_prop.
proof: Proof. unfold absurd_prop in |- *. red in |- *; intros. elim prod_inhabitants with (1 := H0) (a := Srt prop) (b := Ref 0) (3 := H); auto with coc. intros. inversion_clear H1. inversion H2. intros (ty, (M, eq_abs)). rewrite eq_abs in H0. apply inv_typ_abs with (1 := H0); intros. specialize inv_conv_prod_l with (1 := H4); intro conv_ty. specialize inv_conv_prod_r with (1 := H4); intro conv_P. clear H0 H4 H3 H1. cut (is_atom (ty :: nil) M). intros (n, lt_n, (l, eq_atom)). simpl in lt_n. generalize eq_atom. clear eq_atom. replace n with 0; try lia. rewrite <- (rev_involutive l). case (rev l); simpl in |- *; intros; rewrite eq_atom in H2. apply inv_typ_ref with (1 := H2). intros U itm_U. inversion_clear itm_U. intro conv_T. cut (Ref 0 = Srt prop); try discriminate. apply nf_uniqueness. apply trans_conv_conv with T; auto with coc. apply trans_conv_conv with (lift 1 ty); auto with coc. change (conv (lift_rec 1 ty 0) (lift_rec 1 (Srt prop) 0)) in |- *. apply conv_conv_lift; auto with coc. red in |- *; red in |- *; intros r red_n; inversion red_n. red in |- *; red in |- *; intros r red_n; inversion red_n. rewrite applist_assoc in H2. simpl in H2. elim inv_typ_applist_head with (1 := H2); intros. clear H2 eq_atom. apply inv_typ_app with (1 := H0); intros. apply inv_typ_ref with (1 := H1); intros. apply conv_sort_prod with prop V Ur. apply trans_conv_conv with (lift 1 U); auto with coc. apply sym_conv. change (conv (lift_rec 1 U 0) (lift_rec 1 (Srt prop) 0)) in |- *. inversion_clear H4. apply conv_conv_lift; auto with coc. apply atom_inhabitants with (1 := H2) (2 := conv_P). split with 0; simpl in |- *; auto with arith; split with (nil (A:=term)); trivial. apply hnf_proofs_sound with (1 := H2). rewrite eq_abs in H. red in |- *; red in |- *; intros. elim H with (Abs ty u); auto with coc. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia