fact: Hypothesis eq_bool_ok : forall t1 t2, match eq_bool t1 t2 with true => eq_A t1 t2 | false => ~eq_A t1 t2 end.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)