proposition: Lemma app_lift_app_aux : forall M (Mapp: isApp M) n k, isApp (proj1_sig (lift_aux n M k)).
proof: Proof. intros. destruct M as [E Pt T M]; destruct M; try contr. destruct (lift_aux n (buildT (TApp M1 M2))) as [W [WE [WPt WT]]]. apply app_isApp with (prelift_aux n PtL k) (prelift_aux n PtR k); trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)