fact: Definition nb_vars_eq l1 l2 := cardinal (vars_eqns l1) = cardinal (vars_eqns l2).
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)