proposition: Lemma fun_eq_sub f ts s u : Fun f ts = sub s u -> {exists us, u = Fun f us} + {exists x, u = Var x}.
proof: Proof. intro H. destruct u. right. exists n. refl. left. case (eq_symb_dec f f0); intro E. rewrite E. exists t. refl. simpl in H. simplify_eq H. contr. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)