 Timestamp:
 Dec 17, 2012, 2:35:30 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2532 r2557 114 114 qed. 115 115 116 117 116 (* use Russell? *) 118 117 axiom adds_graph_list_ok : … … 126 125 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 127 126 src ~❨b,l❩~> dst in joint_if_code … def'. 128 (* #p #g #l elim l 127 (* 128 #p #g #l elim l l 129 129 [ #src #def #_ #Hdef whd 130 %{Hdef} %{[ ]} %%% 131 #hd #tl #IH #src #def #src_fresh #Hdef132 133 134 135 136 137 138 139 [ cases def //] #EQ_aux130 %{Hdef} %{[ ]} %%% ] 131 #hd #tl #IH #src #def #src_fresh #Hdef 132 whd in match (adds_graph_list ?????); 133 whd in match (fresh_label ???); 134 @(pair_elim … (fresh ??)) normalize nodelta 135 #mid #luniverse' #EQfresh 136 whd in ⊢ (match % with [ _ ⇒ ?]); 137 letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse')) 138 cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def) 139 [ % ] #EQ_aux 140 140 lapply (IH mid def' ??) 141 141 [ #l whd in match def'; #Hpres … … 157 157 % [ % ] 158 158 [ whd in ⊢ (?%); 159 elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta 160 [ elim (All_memb … Hl2 H) 161 cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?); 162 #H #_ @(absurd ?? H) 163 @(fresh_remains_fresh … (eqEQfresh) 159 cut (Not (bool_to_Prop (mid∈l))) 160 [ % #H elim (All_memb … Hl2 H) 161 whd in match (joint_if_luniverse ???); 162 #G #_ @(absurd ?? G) 163 @ (fresh_is_fresh … (sym_eq … EQfresh)) 164  #H >H assumption 165 ] 166  % 167 [ % 168 [ 164 169 normalize #H10 #H11 165 170
Note: See TracChangeset
for help on using the changeset viewer.