diff options
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 3799e38b..4d503f90 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -204,11 +204,6 @@ Proof. Qed. Local Hint Resolve kill_sym_val_referenced : wellformed. -Lemma in_or_not: - forall (x : reg) l, - (In x l) \/ ~(In x l). -Admitted. - Lemma remove_from_sets_notin: forall dst l sets j, not (In j l) -> |