fact: Definition eq_bool (t1 t2 : A) : bool := match t1, t2 with | (true, _), (false, _) => false | (false, _), (true, _) => false | (_, t1), (_, t2) => EqtT.T.F.Symb.eq_bool t1 t2 end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)