fact: Definition step (p : problem) := match p with | Some (l1, e :: l2) => match e with | (v, Var x) => if beq_term v (Var x) then Some (l1, l2) else if mem x (vars v) then None else Some ((x, v) :: List.map (solved_eqn_sub (single x v)) l1, List.map (eqn_sub (single x v)) l2) | (Var x, v) => if beq_term v (Var x) then Some (l1, l2) else if mem x (vars v) then None else Some ((x, v) :: List.map (solved_eqn_sub (single x v)) l1, List.map (eqn_sub (single x v)) l2) | (Fun f vs, Fun g us) => if beq_symb f g then Some (l1, List.combine (list_of_vec vs) (list_of_vec us) ++ l2) else None end | _ => p end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)