fact: Definition EvalInstanceof (e : Expression) (t : StaticType) (st : State.t) : Prop := match EvalRefExpression e st with | None => False | Some l => match Heap.typeof st@h l with | Some lt => lt2t lt = t | None => False end end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)