proposition: Theorem Outof_Into : forall ts T p pf v, @OutOf ts T p pf (@Into ts T p pf v) = Some v.
proof: Proof. Proof using. unfold OutOf, Into. intros. repeat rewrite (eq_Arr_eq pf). repeat rewrite (eq_Const_eq pf). repeat rewrite (eq_Const_eq (eq_sym pf)). unfold asNth. simpl. rewrite asNth'_get_lookup. { generalize dependent (pmap_lookup' ts p). intros. subst. reflexivity. } Qed.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)