Changeset 2286 for src/ASM/Util.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r2211 r2286 1437 1437 interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g). 1438 1438 1439 lemma If_elim : ∀A.∀P : A → Prop.∀b : bool.∀f : b → A.∀g : Not (bool_to_Prop b) → A. 1440 (∀prf.P (f prf)) → (∀prf.P (g prf)) → P (If b then with prf do f prf else with prf do g prf). 1441 #A #P * #f #g #H1 #H2 normalize // qed. 1442 1439 1443 (* Also extracts an equality proof (useful when not using Russell). *) 1440 1444 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
Note: See TracChangeset
for help on using the changeset viewer.