fact: Definition rArrayGetP (ar : rArrayP) (r : rNat) := match ar with | rArrayMakeP t f => match rTreeGetP t r with | PSome a => a | _ => f r end end.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)