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