added general lemmas for strong normalization of untyped lambda terms…

[WegmannDavid]

… and a partially complete proof for strong norm of stlc

[intgrah]

sn_app is relatively straight forward

lemma sn_app (t s : Term Var) :
  SN t →
  SN s →
  (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) →
  SN (t.app s) := by
  intro h_sn_t h_sn_s hβ
  induction h_sn_t generalizing s with | sn t ht ih_t =>
  induction h_sn_s with | sn s hs ih_s =>
  constructor
  intro u hstep
  cases hstep with
  | beta _ _ => apply hβ <;> rfl
  | appL _ h_s_red =>
    apply ih_s _ h_s_red
    intro t' s'' hstep1 hstep2
    exact hβ hstep1 (Relation.ReflTransGen.head h_s_red hstep2)
  | appR _ h_t_red =>
    apply ih_t _ h_t_red _ (SN.sn s hs)
    intro t' s' hstep1 hstep2
    exact hβ (Relation.ReflTransGen.head h_t_red hstep1) hstep2
    ```

[chenson2018]

Is this meant to have some extra hypothesis? It is not true in general as is.

[WegmannDavid]

Yes, this will require another hypothesis, but I was holding that off until later, I am not yet sure exactly how this hypothesis is best formulated. Maybe I should have put in some blank.