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