proposition: Lemma appUnit_env : forall Mu M, isAppUnit Mu M -> env Mu = env M.
proof: Proof. destruct M as [E Pt T M]. induction M; intros; try solve [inversion H; try contr; rewrite <- H0; trivial]. unfold isAppUnit in H. rewrite (appUnits_app (buildT (TApp M1 M2)) I) in H. simpl in H. destruct (in_app_or H). apply IHM1; trivial. inversion H0; try_solve. rewrite <- H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)