proposition: Fact rrmatch {A} f g t : rrspec (A:=A) f g t (rrcase f g t).
proof: Proof. destruct t as [|[|] l x r]; simpl; try now constructor. destruct l as [|[|] ll lx lr], r as [|[|] rl rx rr]; now constructor. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat