fact: Fixpoint o_bool (t1 t2:term) {struct t1} : bool := match t1, t2 with | Var v1, Var v2 => OX.o_bool v1 v2 | Var _, Term _ _ => false | Term _ _, Var _ => true | Term f1 l1, Term f2 l2 => if F.Symb.eq_bool f1 f2 then let o_term_list := (fix o_term_list (l1:list term) : list term -> bool := fun l2 => match l1, l2 with | nil, nil => true | _ :: _, nil => true | nil, _ :: _ => false | h1 :: tl1, h2 :: tl2 => if eq_bool h1 h2 then o_term_list tl1 tl2 else o_bool h1 h2 end) in o_term_list l1 l2 else OF.o_bool f1 f2 end.
imports: Coq(Relations List) CoLoR(list_sort term_spec)