proposition: Lemma vars_eq_sub n s u : Var n = sub s u -> exists m, u = Var m.
proof: Proof. intro. destruct u. exists n0. refl. simpl in H. discr. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)