fact: Fixpoint asNth' {ts : pmap Type} (p p' : positive) : match pmap_lookup' ts p' with | None => Empty_set | Some T => T end -> option (match pmap_lookup' ts p with | None => Empty_set | Some T => T end) := match p as p , p' as p' return match pmap_lookup' ts p' with | None => Empty_set | Some T => T end -> option (match pmap_lookup' ts p with | None => Empty_set | Some T => T end) with | xH , xH => Some | xI p , xI p' => asNth' p p' | xO p , xO p' => asNth' p p' | _ , _ => fun _ => None end.
imports: Coq(PArith) ExtLib.Data.Map.FMapPositive ExtLib.Data.Eq ExtLib.Tactics.Injection Coq(PArith)