-lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/dynamic/nv_drops.ma".
+
+(* NATIVE VALIDITY FOR TERMS ************************************************)
+
+(* Properties with supclosure ***********************************************)
+
+(* Basic_2A1: uses: snv_fqu_conf *)
+lemma nv_fqu_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2