-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.
[ 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
[ 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
- [ 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).
[ 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
[ 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
- [ 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).