search

esum / internship2019

0 stars 0 forks source link

mem_big_eq #4

Open vblot opened 5 years ago

vblot commented 5 years ago

https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/seq2.v#L68 ce lemme peut être prouvé par :

  by move=> x s; rewrite big_has has_pred1.

du coup ce n'est peut-être pas la peine de le prouver séparément.