subst_eqv_head and subst_eqv should be defined using Proposition.equiv first, and then have accompanying theorems for Proposition.Equiv.
|
/- TODO: Proof-relevant substitution principles for logical equivalence in CLL. |
|
|
|
`subst_eqv_head` and `subst_eqv` should be defined using `Proposition.equiv` first, and then |
|
have accompanying theorems for `Proposition.Equiv`. |
|
labels: logic |
|
-/ |
subst_eqv_headandsubst_eqvshould be defined usingProposition.equivfirst, and then have accompanying theorems forProposition.Equiv.cslib/Cslib/Logics/LinearLogic/CLL/Basic.lean
Lines 354 to 359 in 81a21d3