---

Step * of Lemma subtype_rel_dep_function_iff

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (uiff(∀[a:C]. (B[a] ⊆r D[a]);(a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c]))) supposing 
     ((∀x,y:A.  Dec(x = y ∈ A)) and 
     (a:A ⟶ B[a]) and 
     (C ⊆r A))
BY
{ TACTIC:(Auto THEN Try ((DoSubsume THEN Auto THEN BackThruSomeHyp)⋅)) }

1
.....wf..... 
1. A : Type
2. B : A ⟶ Type
3. C : Type
4. D : C ⟶ Type
5. C ⊆r A
6. a:A ⟶ B[a]
7. ∀x,y:A.  Dec(x = y ∈ A)
8. (a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c])
9. a : C
10. x : B a
⊢ x ∈ D a

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].
    (uiff(\mforall{}[a:C].  (B[a]  \msubseteq{}r  D[a]);(a:A  {}\mrightarrow{}  B[a])  \msubseteq{}r  (c:C  {}\mrightarrow{}  D[c])))  supposing 
          ((\mforall{}x,y:A.    Dec(x  =  y))  and 
          (a:A  {}\mrightarrow{}  B[a])  and 
          (C  \msubseteq{}r  A))


By

---

Latex:
TACTIC:(Auto  THEN  Try  ((DoSubsume  THEN  Auto  THEN  BackThruSomeHyp)\mcdot{}))

---

Home Index