proposition: Fact subst_Fr_ {ff} L sigma : map (subst_form sigma) (map (@Fr ff) L) = map Fr (map (subst_form sigma) L).
proof: Proof. induction L. - reflexivity. - cbn. now rewrite IHL, subst_Fr. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)