diff options
| author | Edward Wang | 2020-04-13 18:14:44 -0400 |
|---|---|---|
| committer | Edward Wang | 2020-09-07 02:40:56 +0000 |
| commit | ad89d85911927f0e95df7a72fe51aec0ab964d94 (patch) | |
| tree | d288d0e8226304aa5d899e1d94f21c5470aefe4b /kernel/nativevalues.ml | |
| parent | 48f465dd5c5f9db416a7cd57b0acb86f17323ce3 (diff) | |
Add iff variant for app_inj_tail
The lemma is true in the other direction and can be useful in proofs.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions