proposition: Lemma apps_head_args : forall u, u = apps (head u) (args u).
proof: Proof. induction u; simpl; auto. rewrite IHu1, app_apps, head_apps, head_head, <- IHu1. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)