proposition: Lemma wf_unproj22 : forall (R:binary A2), wf R -> wf (unproj22 A1 R).
proof: Proof. Proof using. intros R H [x1 x2]. gen x1. induction_wf IH: H x2. constructor. intros [y1 y2]. auto. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)