proposition: Lemma supterm_wf : WF supterm.
proof: Proof. apply (WF_incl (Rof Peano.gt size)). induction 1; unfold Rof; simpl; try max; lia. apply WF_inverse. apply WF_gt. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)