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