proposition: Lemma wf_lexico4 : forall A1 A2 A3 A4 (R1:binary A1) (R2:binary A2) (R3:binary A3) (R4:binary A4), wf R1 -> wf R2 -> wf R3 -> wf R4 -> wf (lexico4 R1 R2 R3 R4).
proof: Proof. Proof using. intros. apply~ wf_lexico3. apply~ wf_lexico2. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)