proposition: Lemma logical {X} (P Q : X -> Prop) : (forall x, Q x -> P x) -> ((forall x, Q x -> P x) -> forall x, P x -> Q x) -> forall x, P x <-> Q x.
proof: Proof. firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)