proposition: Lemma csf_wd_unfolded: forall (f : CSetoid_fun) (x y : S1), x[=]y -> f x[=]f y.
proof: Proof. Proof csf_wd. Definition Const_CSetoid_fun : S2 -> CSetoid_fun. Proof. intro c; apply (Build_CSetoid_fun (fun x : S1 => c)); intros x y H. elim (ap_irreflexive _ _ H). Defined.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid