fact: Record CSetoid_relation : Type := {csr_rel :> S -> S -> Prop; csr_wdr : rel_wdr csr_rel; csr_wdl : rel_wdl csr_rel; csr_strext : rel_strext csr_rel}.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid