proposition: Lemma nid_eq_equiv: forall {A} (t1 t2: A) n1 n2, (if n1 =_? n2 then t1 else t2) = (if n1 =? n2 then t1 else t2).
proof: Proof. Proof using. intros. destruct Peano_dec.eq_nat_dec as [Heq | Hneq]; subst; auto. rewrite Nat.eqb_refl; auto. apply Nat.eqb_neq in Hneq; rewrite Hneq; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)