proposition: Lemma normal_abs_inv : forall T M : term, normal (Abs T M) -> normal T /\ normal M.
proof: Proof. unfold normal in |- *; intuition. apply H with (Abs u M); auto with coc. apply H with (Abs T u); auto with coc. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm