proposition: Lemma app_Req_LtypeEq : forall M N (Mapp: isApp M) (Napp: isApp N), term (appBodyR Mapp) = term (appBodyR Napp) -> env M = env N -> type M = type N -> type (appBodyL Mapp) = type (appBodyL Napp).
proof: Proof. intros M N; term_inv M; term_inv N; intros; simpl in * |-. assert (Aeq: type (buildT T2) = type (buildT T4)). auto with terms. simpl in *; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)