proposition: Lemma asNth'_get_lookup : forall p ts v, asNth' (ts:=ts) p p v = Some v.
proof: Proof. induction p; simpl; intros; auto. Qed.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)