proposition: Lemma composeE : forall x m v θ, VM.find x m = Some v -> (m ⊕ θ) x = v.
proof: Proof. by intros x m v θ Hfind; unfold compose; rewrite Hfind. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)