Changeset 2133


Ignore:
Timestamp:
Jun 28, 2012, 10:59:18 AM (5 years ago)
Author:
boender
Message:
  • moved does_not_occur_occur_absurd
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/LabelledObjects.ma

    r1882 r2133  
    137137qed.
    138138
     139lemma does_not_occur_occurs_absurd: ∀tag,A,id,list_instr.
     140  does_not_occur tag A id list_instr = true →
     141  occurs_exactly_once tag A id list_instr = true →
     142  False.
     143 #tag #A #id #list_instr elim list_instr
     144 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS)
     145 | #h #t #Hind whd in match (does_not_occur ????);
     146   whd in match (occurs_exactly_once ????);
     147   cases (instruction_matches_identifier ?? id h) normalize nodelta
     148   [ #ABS destruct (ABS)
     149   | @Hind
     150   ]
     151 ]
     152qed.
     153
     154
    139155let rec index_of_internal A (test : A → bool) (l : list A) acc on l : ℕ ≝
    140156  match l with
Note: See TracChangeset for help on using the changeset viewer.