Ignore:
Timestamp:
Dec 19, 2011, 2:48:37 PM (9 years ago)
Author:
campbell
Message:

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1630 r1631  
    55[ //
    66| #hd #tl #IH #r * #H1 #H2 #H3 % // @IH //
    7 ] qed.
     7] qed.
     8
     9lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l.
     10#A #P #l elim l
     11[ //
     12| #hd #tl #IH #r * #H1 #H2 % /2/
     13] qed.
     14
     15lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r.
     16#A #P #l elim l
     17[ //
     18| #h #t #IH #r * /2/
     19] qed.
    820
    921(* An alternative form of All that can be easier to use sometimes. *)
Note: See TracChangeset for help on using the changeset viewer.