proposition: Lemma pw {X : Type} P Q : (forall x : X, P x <-> Q x) -> (forall x, P x) <-> (forall x, Q x).
proof: Proof. firstorder. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms