proposition: Lemma CType_S : Setoid_Theory [univ] c_t_iff.
proof: Proof. split. repeat constructor; auto. unfold Symmetric; intros. inversion H; subst. dall. repeat constructor; auto. unfold Transitive; intros. inversion H; inversion H0; subst. dall. repeat constructor; auto. Qed.
imports: universe Coq.Setoids.Setoid