proposition: Lemma lift_absBody : forall E Pt A B (M: decl A E |- Pt := B) n k (MLabs: isAbs (proj1_sig (lift_aux n (buildT (TAbs M)) k))), absBody MLabs = proj1_sig (lift_aux n (buildT M) (S k)).
proof: Proof. intros. destruct (lift_aux n (buildT M) (S k)) as [P [Penv [Pterm Ptype]]]. destruct (lift_aux n (buildT (TAbs M)) k) as [Q [Qenv [Qterm Qtype]]]. apply term_eq. rewrite absBody_env. simpl; rewrite Penv; rewrite Qenv. unfold liftedEnv, decl; simpl. replace A with (absType MLabs). unfold finalSeg; trivial. apply abs_type with B; trivial. apply absBody_term with A. simpl; rewrite Qterm; rewrite Pterm; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)