def substitution_lemma (i : Nat) {t t' u u' : Term} (tt' : t ⇛ t') (uu' : u ⇛ u') (min_free_locs_u' : le_nat_option_nat i (min_free_loc 0 u')) : substitute (i, u) t ⇛ substitute (i, u') t'

Substitution Lemma [KS22, Lemma 3.5]

Equations

• One or more equations did not get rendered due to their size.

def substitution_lemma_Lst (i : Nat) {lst : List Attr} {l l' : Bindings lst} (premise : Premise l l') {u u' : Term} (uu' : u ⇛ u') (min_free_locs_u : le_nat_option_nat i (min_free_loc 0 u')) : Premise (substituteLst (i + 1, incLocators u) l) (substituteLst (i + 1, incLocators u') l')

Equations

• One or more equations did not get rendered due to their size.
• substitution_lemma_Lst i Premise.nil uu' min_free_locs_u = id Premise.nil
• substitution_lemma_Lst i (Premise.consVoid a premise_tail) uu' min_free_locs_u = id (Premise.consVoid a (substitution_lemma_Lst i premise_tail uu' min_free_locs_u))