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