Update test outputs

Blaisorblade · Aug 29, 2022 · 6a37432 · 6a37432
1 parent 753affa
commit 6a37432
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/tests/test_used_axioms.ref b/tests/test_used_axioms.ref
@@ -7,6 +7,7 @@ FunctionalExtensionality.functional_extensionality_dep
   : ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
       (∀ x : A, f x = g x) → f = g
 Axioms:
+ProofIrrelevance.proof_irrelevance : ∀ (P : Prop) (p1 p2 : P), p1 = p2
 FunctionalExtensionality.functional_extensionality_dep
   : ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
       (∀ x : A, f x = g x) → f = g