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