proposition: Lemma algebraic_swap_abs : forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP), (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP), subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min -> algebraic P -> algebraic (swap MP)) -> pos <> PThis M -> isAbs M -> ~isFunApp (M // pos) -> algebraic M -> algebraic P -> algebraic (swap MP).
proof: Proof. intros. destruct pos; try_solve. assert (MPabs: isAbs (swap MP)). apply swap_abs. apply AlgAbs with MPabs. destruct (placeHolder_abs MP) as [MPin MPeq]. rewrite <- (swap_in_abs (TAbs AbsB) MPin); trivial. apply H; trivial. change (buildT AbsB) with (@absBody (buildT (TAbs AbsB)) I). apply absBody_subterm. inversion H3; try_solve. rewrite MPeq; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)