proposition: Theorem coc_consistency : forall t, ~ typ nil t absurd_prop.
proof: Proof. red in |- *; intros. elim compute_nf with t; intros. specialize subject_reduction with (1 := p) (2 := H). apply coc_consistency_nf; trivial. apply str_norm with (1 := H). Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia