Changeset 2642


Ignore:
Timestamp:
Feb 7, 2013, 3:24:50 PM (6 years ago)
Author:
piccolo
Message:

fixed joint/Traces after having posed block 0 to be Code

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2638 r2642  
    9696  ].
    9797cases m0 in H; #m1 #m2 #m3 #H
    98 whd in H:(???%); destruct whd in ⊢(??%?); @Zltb_elim_Type0 // #abs @⊥
    99 @(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by transitive_Zlt/
     98whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
     99@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/
    100100qed.
    101101
Note: See TracChangeset for help on using the changeset viewer.