proposition: Lemma algebraic_swap : forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP), ~isFunApp (M // pos) -> algebraic M -> algebraic P -> algebraic (swap MP).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP), ~isFunApp (M // pos) -> algebraic M -> algebraic P -> algebraic (swap MP)). apply subterm_wf. clear M; intros M IH pos MP P Mnfa Malg Palg. induction pos. apply algebraic_swap_this; trivial. apply algebraic_swap_abs; try_solve. apply algebraic_swap_app; try_solve. apply algebraic_swap_app; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)