daily pastebin goal
6%
SHARE
TWEET

Untitled

a guest Jul 9th, 2017 63 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  1.      (thm : (x : (P : ∗¹)
  2.                  (foo_ : (barfoo_ : A⇧¹)(baz_ : A⇧¹) → P)
  3.                  P)
  4.             (y : (P : ∗¹)(foo_ : (barfoo_ : A⇧¹)(baz_ : A⇧¹) → P) → P)
  5.             ((P₁ : ∗¹)
  6.              (fooP₁ : ∗¹)
  7.              (P : (foo_ : P₁)(bar_ : fooP₁) → ∗)
  8.              (_₁ : (foo_ : A⇧¹)(bar_ : A⇧¹) → P₁)
  9.              (bar_₁ : (foo_ : A⇧¹)(bar_ : A⇧¹) → fooP₁)
  10.              (baz_ : (foo_₁ : A⇧¹)
  11.                      (bazbar_₁ : A⇧¹)
  12.                      (foobar_ : A!!%² foo_₁ bazbar_₁)
  13.                      (fubar_₁ : A⇧¹)
  14.                      (qux_₁ : A⇧¹)
  15.                      (quux_ : A!!%² fubar_₁ qux_₁)
  16.                      P (_₁ foo_₁ fubar_₁) (bar_₁ bazbar_₁ qux_₁))
  17.              P (x P₁ _₁) (y fooP₁ bar_₁))
  18.             A!!%² (f⇧¹ x) (f⇧¹ y)) ×
  19.      ∗₁
  20.  
  21.  
  22.  (thm : (x : (P : ∗¹)(A⇧¹ → A⇧¹ → P) → P)
  23.         (y : (P : ∗¹)(A⇧¹ → A⇧¹ → P) → P)
  24.         ((P₁ : ∗¹)
  25.          (P₁ : ∗¹)
  26.          (P : P₁ → P₁ → ∗)
  27.          (_₁ : A⇧¹ → A⇧¹ → P₁)
  28.          (_₁ : A⇧¹ → A⇧¹ → P₁)
  29.          ((_₁ : A⇧¹)
  30.           (_₁ : A⇧¹)
  31.           A!!%² _₁ _₁ →
  32.           (_₁ : A⇧¹)
  33.           (_₁ : A⇧¹)
  34.           A!!%² _₁ _₁ →
  35.           P (_₁ _₁ _₁) (_₁ _₁ _₁))
  36.          P (x P₁ _₁) (y P₁ _₁))
  37.         A!!%² (f⇧¹ x) (f⇧¹ y)) ×
  38.  ∗₁
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top