proposition: Fact rrmatch' {A} f g m : rrspec (A:=A) f g m (rrcase' f g m).
proof: Proof. unfold rrcase'. destmatch; now constructor. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)