#u1; #dim1;
#y; nelim y;
#u2; #dim2;
- nchange with (? → eqc ? u1 u2 = true);
+ nchange with (? → (eqc ? u1 u2) = true);
#H; napply (eq_to_eqc ? u1 u2);
napply (SUN_destruct_1 l … H).
nqed.
nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
#l; #x; #y;
- nchange with ((eqc ? (getelem ? x) (getelem ? y) = true) → x = y);
+ nchange with (((eqc ? (getelem ? x) (getelem ? y)) = true) → x = y);
#H; napply (eqSUN_to_eq_aux l x y (eqc_to_eq … H)).
nqed.
| ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
].
-nlemma farg1_auxDim : ∀h,t,x.eqc ? x h = false → member_natList x (h§§t) = true → member_natList x t = true.
+nlemma farg1_auxDim : ∀h,t,x.(eqc ? x h) = false → member_natList x (h§§t) = true → member_natList x t = true.
#h; #t; #x; #H; #H1;
nnormalize in H1:(%);
nrewrite > H in H1:(%);
[ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
| ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
match eqc ? (getelem ? x) h
- return λy.eqc ? (getelem ? x) h = y → ?
+ return λy.(eqc ? (getelem ? x) h) = y → ?
with
- [ true ⇒ λp:(eqc ? (getelem ? x) h = true).fst … arg
- | false ⇒ λp:(eqc ? (getelem ? x) h = false).
+ [ true ⇒ λp:((eqc ? (getelem ? x) h) = true).fst … arg
+ | false ⇒ λp:((eqc ? (getelem ? x) h) = false).
farg1 T t
(snd … arg)
(S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
[ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
| ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
match eqc ? (getelem ? x) h
- return λy.eqc ? (getelem ? x) h = y → ?
+ return λy.(eqc ? (getelem ? x) h) = y → ?
with
- [ true ⇒ λp:(eqc ? (getelem ? x) h = true).farg1 T lfix (fst … arg)
- | false ⇒ λp:(eqc ? (getelem ? x) h = false).
+ [ true ⇒ λp:((eqc ? (getelem ? x) h) = true).farg1 T lfix (fst … arg)
+ | false ⇒ λp:((eqc ? (getelem ? x) h) = false).
farg2 T t lfix
(snd … arg)
(S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))