proposition: Lemma algebraic_swap_app : 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 -> ~isFunApp (M // pos) -> isApp M -> algebraic M -> algebraic P -> algebraic (swap MP).
proof: Proof. intros. destruct (isFunApp_dec M). apply AlgFunApp; trivial. apply swap_isFunApp; trivial. rewrite swap_type_eq. inversion H3; term_inv M. intros. apply (algebraic_swap_isFunApp MP); trivial. inversion H3; term_inv M. apply AlgApp; trivial. apply app_swap_app; trivial. apply swap_not_funApp; trivial. fold P; inversion H4; term_inv P. intros. apply (algebraic_swap_notFunApp MP); trivial. inversion H3; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)