]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma
uncommited file found :)
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / ltpss_sn_alt.ma
index 8b414d2030b401f9f8b88c727c1aeac57492bd3e..d2cdba023c7baa581f5df8f3866ea4a4fe4a4bdd 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+
 include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
 include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".