(* *)
(**************************************************************************)
+include "basic_2/notation/relations/unfold_3.ma".
include "basic_2/grammar/lenv_append.ma".
include "basic_2/relocation/ldrop.ma".
.
interpretation "context-sensitive unfold (term)"
- 'Unwind L1 T L2 = (unfold L1 T L2).
+ 'Unfold L1 T L2 = (unfold L1 T L2).