fact: Fixpoint well_formed (t:term) : Prop := match t with | Var _ => True | Term f l => let well_formed_list := (fix well_formed_list (l:list term) : Prop := match l with | nil => True | h :: tl => well_formed h /\ well_formed_list tl end) in well_formed_list l /\ (match arity f with | Free n => length l = n | _ => length l = 2 end) end.
imports: List more_list list_permut list_set Arith