Type theory and propositions as types

Under the propositions-as-types correspondence, what is a proof of $A \wedge B$?

What is the most general simple type of $\lambda f.\, \lambda g.\, \lambda x.\, f\,(g\, x)$, and hence which tautology does it prove?

Which of these types are inhabited by a closed term (equivalently, are theorems of intuitionistic propositional logic)? Here $p, q$ are base types and $\neg A = A \to 0$. Choose all that apply.

In the two-state Kripke model $w_0 \le w_1$ with $p$ known only at $w_1$, which formulas are forced at $w_0$? (Rules: $w \Vdash A \to B$ iff every $v \ge w$ forcing $A$ forces $B$; $\bot$ is forced nowhere, $\neg A = A \to \bot$; $w \Vdash A \vee B$ iff $w \Vdash A$ or $w \Vdash B$.) Choose all that apply.

Let $A$ be a base type. How many closed β-normal terms of type $A \to A \to A$ are there (counting α-equivalent terms once)?

In the proof of soundness for Kripke models (Theorem 3), the $\to$-introduction case goes: assume $w$ forces all of $\Gamma$, let $v \ge w$ force $A$; then $v$ forces all of $\Gamma, A$, so $v \Vdash B$ by induction. Which fact justifies '$v$ forces all of $\Gamma$'?

With addition on $\N$ defined by $m + \mathsf{zero} = m$ and $m + \mathsf{succ}\, n = \mathsf{succ}(m + n)$, why is $n + 0 = n$ true by computation while $0 + n = n$ needs induction?

The lesson's Lean file proves both peirce_classical (A B : Prop) : ((A → B) → A) → A and peirce_uninhabited : ¬ ∃ t, HasType [] t (((Ty.base 0 ⇒ Ty.base 1) ⇒ Ty.base 0) ⇒ Ty.base 0). Why is this not a contradiction?

Write forces(w, f, le, val) for implicational formulas in a finite Kripke model. A formula is either an atom (a string such as 'p') or a tuple ('imp', A, B). le is a set of pairs (u, v) meaning $u \le v$ (reflexive and transitive), and val[w] is the set of atoms known at w. Use: atoms are forced when known; ('imp', A, B) is forced at w iff every v with (w, v) in le that forces A also forces B.