2c989ceb · mp done

91ad0ec1 · simplifying pp

f1b5328f · on pp

4bade050 · updated bij_list

d24124bc · bij_permut_list is bij_subset...

497f90e0 · nothing

4ca3770e · simpl proofs

9de7606e · tp cong simpl

977dc2df · simpled tp left neutral proof

d1c14eb3 · bunfold tact

f3583c54 · fixed myeqnat to be with no constructor removing the need for destr...

337d7f76 · fully removed switch_link

333db36e · changed order of link function so that switch_link is no longer needed

a21af145 · tryig to simp not_is_idle_imp port part

57e3f8c3 · imp and is_imp need improving

bd81b5b7 · refactored AGAIN se imp lse less than 100 lines now!

8b60868d · lse in a equiv

d3909429 · lse pas trop trivial l'equivalence

3f1e1051 · raccourci seimpllse

ae47fbb7 · small changes