Changeset 1516 for src/ASM/Status.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Status.ma
r1515 r1516 916 916 @ le_S_S 917 917 lapply (le_n n) 918 generalize in ⊢ (?%? → ?(??%?)?) 919 elim n in ⊢ (∀_:?. ??% → ?(?%??)?) 918 generalize in ⊢ (?%? → ?(??%?)?); 919 elim n in ⊢ (∀_:?. ??% → ?(?%??)?); 920 920 [ normalize 921 921 #n … … 924 924 [ // 925 925 | #H #K 926 inversion K926 @(le_inv_ind ?? K …) 927 927 [ # H1 928 928 < H1 … … 946 946 # x # K1 947 947 lapply (le_S_S_to_le … K1) 948 generalize in match m 948 generalize in match m; 949 949 elim x 950 950 normalize … … 955 955 // 956 956 # q # K2 957 applyH957 @H 958 958 /3/ 959 959 ]
Note: See TracChangeset
for help on using the changeset viewer.