proposition: Lemma OUTL_def {A B : Type'} : (@OUTL A B) = (@ε ((prod nat (prod nat (prod nat nat))) -> (sum A B) -> A) (fun OUTL' : (prod nat (prod nat (prod nat nat))) -> (sum A B) -> A => forall _17649 : prod nat (prod nat (prod nat nat)), forall x : A, (OUTL' _17649 (@inl A B x)) = x) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))))))).
proof: Proof. exact (eq_refl (@OUTL A B)). Qed.
imports: coq theory_hol types