let and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q) := fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2) in (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro)) : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q)
let1.lean:17:20: error: type mismatch at application
    (fun (and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p)), (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro))) (fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2))
expected type:
    Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p)
given type:
    Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c