proposition: Lemma pred_ext_nondep_4 : forall A1 A2 A3 A4 (P Q : A1 -> A2 -> A3 -> A4 -> Prop), (forall x1 x2 x3 x4, P x1 x2 x3 x4 <-> Q x1 x2 x3 x4) -> P = Q.
proof: Proof. Proof using. intros. apply~ pred_ext_4. Qed.
imports: TLC(LibTactics LibAxioms)