aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0
diff options
context:
space:
mode:
authorEdward Wang2020-04-13 18:14:44 -0400
committerEdward Wang2020-09-07 02:40:56 +0000
commitad89d85911927f0e95df7a72fe51aec0ab964d94 (patch)
treed288d0e8226304aa5d899e1d94f21c5470aefe4b /doc/plugin_tutorial/tuto0
parent48f465dd5c5f9db416a7cd57b0acb86f17323ce3 (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 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions