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