Comment: Hypothesis Subsumption with pointwise
The rule is
  H x:A, J ⊢ C ext t

  BY hypothesis_subsumption #$i B ()    H ⊢ B ⊆r A  H x:A, J ⊢ x ∈ B  H x:B, J ⊢ C ext t (Note that from this rule we can derive the rule hyp_replacement  so that rule could be removed if we rewrite a few tactics.) Here is the proof that the rule is correct (using pointwise functionality)  Let Gamma_A be the hypotheses H x:A J, and Gamma_B be H x:B J.  Let s be a substitution for the variables declared in Gamma.  A substitution s' "agrees with s mod Gamma" if for each v:T in Gamma,  s'(v) = s(v) \in s(T)  s satisfies Gamma if for each v:T in Gamma  s(v) in s(T) and for any s' that agrees with s mod Gamma,   s'(T) = s(T) in some universe Ui.  s satisfies the conclusion (C ext t) if  s(t) in s(C) and for any s' that agrees with s mod Gamma,  s'(C) = s(C) in some universe  A sequent is true if every s that satisfies its hyps also  satisfies its concl.    Assuming that the three subgoal sequents are true we must show that  if s satisfies Gamma_A then s satisfies (C ext t)  Since H x:B, J ⊢ C ext t is assumed true, it is enough to show  s satisfies Gamma_B.  Since s satisfies Gamma_A, it is enough to show that  1) s(x) in s(B) and   2) for any s' that agrees with s mod Gamma_B, for each v:T in Gamma_B   s'(T) = s(T) in some universe.  From the truth of H x:A, J ⊢ x ∈ B we get  Ax \in s(x ∈ B)   and for any s' that agrees with s mod Gamma  s'(x ∈ B) = s'(x ∈ B) in some universe  The first of these implies that s(x) \in s(B), so we have 1)  For 2) it is enough to show that if s' agrees with s mod Gamma_B  then s' agrees with s mod Gamma_A  and s'(B) = s(B) in some universe  For that, suppose s' agrees with s mod Gamma_B. Then s' agrees with s mod H  so since H ⊢ B ⊆r A is true,  Ax \in s(B ⊆r A) and s'(B ⊆r A) = s(B ⊆r A) in some universe  The second of these implies that s'(B) = s(B)  and the first implies that since s'(x) = s(x) \in s(B) then  s'(x) = s(x) \in s(A), so s' agrees with s mod Gamma_A  .  QED  .  ⋅ Comment: Hypothesis Subsumption with pairwise In pairwise functionality, the rule is simpler than in pointwise functionality since we don't need to prove H ⊢ B ⊆r A. The rule becomes:  H x:A, J ⊢ C ext t  BY hypothesis_subsumption #$i B ()

  H x:A, J ⊢ x ∈ B
  H x:B, J ⊢ C ext t

Here is the proof:
  Let Gamma be the hypotheses  H x:A J,  and Gamma' be  H x:B J.
  Let s1, s2 be substitutions for the variables declared in Gamma.

  The pair s1,s2 satisfies Gamma if for each v:T in Gamma
  s1(v) = s2(v) in s1(T)  and  s1(T) = s2(T) in some universe Ui.

  The pair s1,s2 satisfies the conclusion (C ext t) if
  s1(t) = s2(t) in s1(C) and  s1(C) = s2(C) in some universe

  A sequent is true in pairwise functionality
  if every pair s1,s2 that satisfies its hyps also
  satisfies its concl.

  Assuming that the two subgoal sequents are true (in pairwise functionality)
  we must show that
  if s1,s2 satisfies Gamma then s1,s2 satisfies (C ext t)

   Since H x:B, J ⊢ C ext t is assumed true, it is enough to show
   s1,s2 satisfies Gamma'.

   Since s1,s2 satisfy Gamma, it is enough to show that
   s1(x) = s2(x) in s1(B)  and  s1(B) = s2(B) in some universe.

   From the truth of H x:A, J ⊢ x ∈ B  we get
    Ax \in s1(x ∈ B) and s1(x ∈ B) = s2(x ∈ B) in some universe

  This implies that  s1(x) = s2(x) in s1(B) and that
        s1(B) = s2(B) in that universe .
  QED
.

 ⋅

Lemma: sq_stable__subtype_rel
∀[A,B:Type].  SqStable(A ⊆r B)

Lemma: subtype_rel_universe1
Type ⊆r 𝕌'

Lemma: subtype_rel_universe2
Type ⊆r 𝕌''

Lemma: subtype_rel_function
∀[A,B,C,D:Type].  ((A ⟶ B) ⊆r (C ⟶ D)) supposing ((B ⊆r D) and (C ⊆r A))

Lemma: subtype_rel_dep_function
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  ((a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c])) supposing ((∀a:C. (B[a] ⊆r D[a])) and (C ⊆r A))

Lemma: subtype_rel_product
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  ((a:A × B[a]) ⊆r (c:C × D[c])) supposing ((∀a:A. (B[a] ⊆r D[a])) and (A ⊆r C))

Lemma: subtype_rel_image
∀[A,B:Type]. ∀[f:Base].  Image(A,f) ⊆r Image(B,f) supposing A ⊆r B

Lemma: subtype_rel_tunion
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (⋃a:A.B[a] ⊆r ⋃c:C.D[c]) supposing ((∀a:A. (B[a] ⊆r D[a])) and (A ⊆r C))

Lemma: subtype_rel_simple_product
∀[A,B,C,D:Type].  ((A × B) ⊆r (C × D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_union
∀[A,B,C,D:Type].  ((A + B) ⊆r (C + D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_dep_product_iff
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  uiff(∀[a:A]. (B[a] ⊆r D[a]);(a:A × B[a]) ⊆r (c:C × D[c])) supposing A ⊆r C

Lemma: subtype_rel_sum
∀[A,B,C,D:Type].  ((A + B) ⊆r (C + D)) supposing ((B ⊆r D) and (A ⊆r C))

Lemma: subtype_rel_set
∀[A,B:Type]. ∀[P:A ⟶ ℙ].  {a:A| P[a]}  ⊆r B supposing A ⊆r B

Lemma: subtype_rel_set_simple
∀[A:Type]. ∀[P:A ⟶ ℙ].  ({a:A| P[a]}  ⊆r A)

Lemma: subtype_rel_sets
∀[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  ({a:A| P[a]}  ⊆r {b:B| Q[b]} ) supposing ((∀a:A. (P[a]  Q[a])) and ({a:A| P[a]\000C}  ⊆r B))

Lemma: subtype_rel_sets_simple
∀[A:Type]. ∀[P,Q:A ⟶ ℙ].  {a:A| P[a]}  ⊆r {b:A| Q[b]}  supposing ∀a:A. (P[a]  Q[a])

Lemma: subtype_rel_transitivity
∀[A,B,C:Type].  (A ⊆r C) supposing ((B ⊆r C) and (A ⊆r B))

Lemma: subtype_rel_nested_set
∀[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  A ⊆r {b:{b:B| P[b]} | Q[b]}  supposing A ⊆r {b:B| P[b] ∧ Q[b]}

Lemma: subtype_rel_nested_set2
∀[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  {b:{b:B| P[b]} | Q[b]}  ⊆r A supposing {b:B| P[b] ∧ Q[b]}  ⊆r A

Lemma: subtype_rel_isect_general
∀[A,T:Type]. ∀[C:A ⟶ Type]. ∀[B:T ⟶ Type].  (⋂x:A. C[x]) ⊆r (⋂x:T. B[x]) supposing (T ⊆r A) ∧ (∀x:T. (C[x] ⊆r B[x]))

Lemma: subtype_rel_isect
∀[A,T:Type]. ∀[B:T ⟶ Type].  uiff(A ⊆r (⋂x:T. B[x]);∀[x:T]. (A ⊆r B[x]))

Lemma: subtype_rel_isect_as_subtyping_lemma
∀[A,T:Type]. ∀[B:T ⟶ Type].  A ⊆r (⋂x:T. B[x]) supposing ∀[x:T]. (A ⊆r B[x])

Lemma: subtype_rel_isect-2
∀[A:Type]. ∀[B1,B2:A ⟶ Type].  (⋂x:A. B1[x]) ⊆r (⋂x:A. B2[x]) supposing ∀[x:A]. (B1[x] ⊆r B2[x])

Lemma: subtype_rel_double_isect
∀[A,T1,T2:Type]. ∀[B:T1 ⟶ T2 ⟶ Type].  uiff(A ⊆r (⋂x:T1. ⋂y:T2.  B[x;y]);∀[x:T1]. ∀[y:T2].  (A ⊆r B[x;y]))

Lemma: subtype_rel_not
∀[P,Q:ℙ].  (¬P) ⊆r (¬Q) supposing Q  (↓P)

Lemma: isect_subtype_rel_trivial
∀[A,C:Type]. ∀[B:A ⟶ Type].  (⋂x:A. B[x]) ⊆r C supposing ∃x:A. (B[x] ⊆r C)

Lemma: isect_subtype_rel
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:A].  ((⋂x:A. B[x]) ⊆r B[x])

Lemma: double_isect_subtype_rel
∀[T1,T2:Type]. ∀[B:T1 ⟶ T2 ⟶ Type]. ∀[x:T1]. ∀[y:T2].  ((⋂x:T1. ⋂y:T2.  B[x;y]) ⊆r B[x;y])

Definition: rev_subtype_rel
A ⊇r B ==  B ⊆r A

Lemma: rev_subtype_rel_wf
∀[A,B:Type].  (A ⊇r B ∈ ℙ)

Definition: ext-eq
A ≡ B ==  (A ⊆r B) ∧ (B ⊆r A)

Lemma: ext-eq_wf
∀[A,B:Type].  (A ≡ B ∈ ℙ)

Lemma: sq_stable__ext-eq
∀[A,B:Type].  SqStable(A ≡ B)

Lemma: ext-eq_weakening
∀[A,B:Type].  A ≡ B supposing A = B ∈ Type

Lemma: ext-eq_inversion
∀[A,B:Type].  B ≡ A supposing A ≡ B

Lemma: ext-eq_transitivity
∀[A,B,C:Type].  (A ≡ C) supposing (B ≡ C and A ≡ B)

Lemma: iff_weakening_ext-eq
∀[A,B:Type].  {A ⇐⇒ B} supposing A ≡ B

Lemma: subtype_rel_functionality_wrt_iff
∀[A,B,C,D:Type].  ({uiff(A ⊆r B;C ⊆r D)}) supposing (B ≡ D and A ≡ C)

Lemma: subtype_rel_functionality_wrt_implies
∀[A,B,C,D:Type].  ({C ⊆r D supposing A ⊆r B}) supposing ((B ⊆r D) and (A ⊇r C))

Lemma: subtype_rel_weakening
∀[A,B:Type].  A ⊆r B supposing A ≡ B

Lemma: rev_subtype_rel_weakening
∀[A,B:Type].  A ⊇r B supposing A ≡ B

Lemma: subtype-top
∀[T:Type]. uiff(T ⊆r Top;True)

Lemma: subtype_rel-equal
∀[A,B:Type].  A ⊆r B supposing A = B ∈ Type

Lemma: subtype_rel_self
∀[A:Type]. (A ⊆r A)

Lemma: void-product
∀[T,S:Type].  T × S ≡ Void supposing S ≡ Void

Lemma: void-dep-product
∀[S:Type]. ∀[F:S ⟶ Type].  m:S × (F m) ≡ Void supposing S ≡ Void

Lemma: product_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  ((a:A × B[a]) ⊆r Base) supposing ((∀a:A. (B[a] ⊆r Base)) and (A ⊆r Base))

Lemma: simple-product_subtype_base
∀[A,B:Type].  ((A × B) ⊆r Base) supposing ((B ⊆r Base) and (A ⊆r Base))

Lemma: union_subtype_base
∀[A,B:Type].  ((A + B) ⊆r Base) supposing ((B ⊆r Base) and (A ⊆r Base))

Lemma: set_subtype_base
∀[A:Type]. ∀[P:A ⟶ ℙ].  {a:A| P[a]}  ⊆r Base supposing A ⊆r Base

Lemma: isect_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  (⋂a:A. B[a]) ⊆r Base supposing ∃a:A. (B[a] ⊆r Base)

Lemma: tunion_subtype_base
∀[A:Type]. ∀[B:A ⟶ Type].  ⋃a:A.B[a] ⊆r Base supposing ∀a:A. (B[a] ⊆r Base)

Lemma: baseof_subtype
∀[T:Type]. (baseof(T) ⊆r T)

Lemma: baseof_subtype_base
∀[T:Type]. (baseof(T) ⊆r Base)

Lemma: subtype_top
∀[T:Type]. (T ⊆r Top)

Lemma: uall_instance_test
∀[F:Type ⟶ ℤ ⟶ ℤ ⟶ ℙ]. ∀x:∀[A:Type]. ∀[m,c:ℤ].  F[A;m;c]. ∀B:Type. ∀n,b:ℤ.  (x ∈ F[B;n;b])

Lemma: tunion-is-image
∀[A:Type]. ∀[B:A ⟶ Type].  (⋃a:A.B[a] ~ Image((a:A × B[a]),(λp.(snd(p)))))

Lemma: set-is-image
∀[A:Type]. ∀[B:A ⟶ Type].  {a:A| B[a]}  ≡ Image((a:A × B[a]),(λp.(fst(p))))

Lemma: equal_functionality_wrt_subtype_rel
∀[A,B:Type]. ∀[x,y:A].  {x = y ∈ B supposing x = y ∈ A} supposing A ⊆r B

Lemma: equal_functionality_wrt_subtype_rel2
∀[A,B:Type]. ∀[x,y:A].  {(x = y ∈ A)  (x = y ∈ B)} supposing A ⊆r B

Lemma: decidable-subtype
∀[P,Q:ℙ].  (Dec(P) ⊆r Dec(Q)) supposing ((Q  P) and (P ⊆r Q))

Lemma: subtype-respects-equality
∀[A,B:Type].  respects-equality(B;A) supposing B ⊆r A

Lemma: general-subtype-respects-equality
∀[A,B,C:Type].  (respects-equality(B;C)) supposing (respects-equality(A;C) and (B ⊆r A))

Lemma: subtype-base-respects-equality
∀[A,B:Type].  respects-equality(B;A) supposing B ⊆r Base

Home Index