Mercurial > hg > Members > kono > Proof > ZF-in-agda
view .hgtags @ 59:d13d1351a1fa
lemma = cong₂ (λ x not → minimul x not ) oiso { }6
Cannot instantiate the metavariable _1342 to solution (x == od∅ →
⊥) since it contains the variable x which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 May 2019 05:46:05 +0900 |
| parents | 4fb2a239061d |
| children | 94c796aee319 |