fact: Definition rArraySet (ar : rArray) (r : rNat) (v : A) := match ar with | rArrayMake t f => rArrayMake (rTreeSet t r v) f end.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)