proposition: Lemma LocInObj_ObjSet: forall loc obj objs, LocInObj loc obj = true -> ObjSet.In obj objs -> LocInObjSet loc objs = true.
proof: Proof. intros. unfold LocInObj in H. unfold LocInObjSet. destruct loc. inversion H. destruct (ObjDec.eq_dec o). unfold ObjDec.eq in e. subst. apply ObjSet.mem_1;trivial. inversion H. destruct (ObjDec.eq_dec o). unfold ObjDec.eq in e. subst. apply ObjSet.mem_1;trivial. inversion H. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)