# HG changeset patch
# User lcp
# Date 788196506 -3600
# Node ID 190974c664a381010ffd39d9dd7fd4ad9ae18cc9
# Parent  76d9575950f2a3fd03bea77c4c7797c35451316c
inj_apply_equality: new

diff -r 76d9575950f2 -r 190974c664a3 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Dec 23 16:27:45 1994 +0100
+++ b/src/ZF/Perm.ML	Fri Dec 23 16:28:26 1994 +0100
@@ -63,6 +63,10 @@
 by (fast_tac ZF_cs 1);
 qed "inj_equality";
 
+goalw thy [inj_def] "!!A B f. [| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
+by (fast_tac ZF_cs 1);
+val inj_apply_equality = result();
+
 (** A function with a left inverse is an injection **)
 
 val prems = goal Perm.thy
@@ -122,6 +126,10 @@
 by (assume_tac 1);
 qed "id_type";
 
+goalw Perm.thy [id_def] "!!A x. x:A ==> id(A)`x = x";
+by (asm_simp_tac ZF_ss 1);
+val id_conv = result();
+
 val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
 by (rtac (prem RS lam_mono) 1);
 qed "id_mono";