proposition: Lemma lift_appBodyL : forall E PtL PtR A B n k (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A) (MLapp: isApp (proj1_sig (lift_aux n (buildT (TApp Ml Mr)) k))), appBodyL MLapp = proj1_sig (lift_aux n (buildT Ml) k).
proof: Proof. intros. destruct (lift_aux n (buildT (TApp Ml Mr)) k) as [P [PE [PPt PA]]]. destruct (lift_aux n (buildT Ml) k) as [Q [QE [QPt QA]]]. apply term_eq. rewrite appBodyL_env. simpl; rewrite QE; rewrite PE; trivial. simpl; rewrite QPt; simpl. apply appBodyL_term with (prelift_aux n PtR k). rewrite PPt; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)