proposition: Lemma C_ext : Proper (pointwise_relation _ eq ==> eq ==> eq ==> iff) C.
proof: Proof. split; repeat intros ?; subst. now rewrite <- H. now rewrite H. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms