proposition: Lemma domain_fun_transp s : transpose Equal (domain_fun s).
proof: Proof. intros x y xs. unfold Def.domain_fun, bool_of_rel. destruct (eq_term_dec (s x) (Var x)); destruct (eq_term_dec (s y) (Var y)); try refl. apply add_add. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)