include "basic_2/dynamic/lsubsv.ma".
(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2
include "basic_2/dynamic/lsubsv.ma".
(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2