proposition: Lemma lookup_deterministic: forall p cn msig r r', lookup p cn msig r -> lookup p cn msig r' -> r = r'.
proof: Proof. intros. induction H. inversion H0. subst; rewrite H in H1; inversion H1; trivial. rewrite H in H1; inversion H1. inversion H0. rewrite H3 in H; inversion H. apply IHlookup; clear IHlookup. inversion H1; inversion H4. rewrite H10 in H7. inversion H9; inversion H12. unfold PROG.defined_Class in H13, H16. rewrite H7 in H16; rewrite H16 in H13; inversion H13. rewrite H20 in H18; rewrite H18 in H15; inversion H15. rewrite H21 in H11; rewrite <- H11 in H8; rewrite H8. trivial. Qed.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)