Lines Matching refs:h3
915 >> rename[`GROUP_BY R (h3::t2) = h4::t3`]
916 >- (`R h3 y` by (
918 >> Cases_on `SPAN (R h3) t2` >> fs[]
919 >> `!x. MEM x (FST (q,r)) ==> (R h3 x)`
921 >> Cases_on `y = h3` >> fs[]
927 >- (`P h3 H` by (
928 Cases_on `y = h3` >> rw[]
932 `FLAT (GROUP_BY R (h3::t2)) = h3::t2`
934 >> `MEM y (FLAT (GROUP_BY R (h3::t2)))` by (
937 >> `MEM y (h3::t2)` by metis_tac[]
940 >> `P h3 y` by metis_tac[SORTED_EQ]
1077 rename[`GROUP_BY R (h::h1::t) = h3::t2`]
1078 >> first_x_assum (qspec_then `h3` mp_tac)
1114 >- (rename[`GROUP_BY R (h::h1::t) = h3::t2`]
1115 >> first_x_assum (qspec_then `h3` mp_tac)
1149 >- (rename[`GROUP_BY R (h::h1::t) = h3::t2`]
1150 >> first_x_assum (qspec_then `h3` mp_tac)