proposition: Lemma TypeC_S : Setoid_Theory [univ] t_c_iff.
proof: Proof. split. repeat constructor; auto. unfold Symmetric; intros. destruct H. inversion H; subst. inversion H0; subst. repeat constructor; auto. unfold Transitive; intros. destruct H; destruct H0. inversion H; inversion H0; inversion H1; inversion H2; subst. repeat constructor; auto. Qed.
imports: universe Coq.Setoids.Setoid