include "basic_2/computation/dxprs_aaa.ma".
include "basic_2/equivalence/cpcs_aaa.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
include "basic_2/computation/dxprs_aaa.ma".
include "basic_2/equivalence/cpcs_aaa.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)