fact: Fixpoint rTreeSetP (t : rTreeP) (r : rNat) {struct r} : Prop -> rTreeP := fun a : Prop => match r, t with | BinPos.xH, rEmptyP => rSplitP (PSome a) rEmptyP rEmptyP | BinPos.xO p, rEmptyP => rSplitP PNone (rTreeSetP rEmptyP p a) rEmptyP | BinPos.xI p, rEmptyP => rSplitP PNone rEmptyP (rTreeSetP rEmptyP p a) | BinPos.xH, rSplitP _ t'1 t'2 => rSplitP (PSome a) t'1 t'2 | BinPos.xO p, rSplitP b t'1 t'2 => rSplitP b (rTreeSetP t'1 p a) t'2 | BinPos.xI p, rSplitP b t'1 t'2 => rSplitP b t'1 (rTreeSetP t'2 p a) end.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)