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