fact: Fixpoint rTreeSet (t : rTree) (r : rNat) {struct r} : A -> rTree := fun a : A => match r, t with | xH, rEmpty => rSplit (Some a) rEmpty rEmpty | xO p, rEmpty => rSplit (None) (rTreeSet rEmpty p a) rEmpty | xI p, rEmpty => rSplit (None) rEmpty (rTreeSet rEmpty p a) | xH, rSplit _ t'1 t'2 => rSplit (Some a) t'1 t'2 | xO p, rSplit b t'1 t'2 => rSplit b (rTreeSet t'1 p a) t'2 | xI p, rSplit b t'1 t'2 => rSplit b t'1 (rTreeSet t'2 p a) end.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)