proposition: Lemma machineE xs s vs y : machine (closure xs s) vs y -> match s with | var 0 => match xs with | x :: xs => machine x vs y | _ => False end | var (S n) => match xs with | x :: xs => machine (closure xs (var n)) vs y | _ => False end | app s t => machine (closure xs s) ((true, (closure xs t)) :: vs) y | lam s => match vs with | (true, z) :: vs => machine z ((false, (closure xs s)) :: vs) y | (false, (closure x's s')) :: vs => machine (closure ((closure xs (lam s)) :: x's) s') vs y | nil => True end end.
proof: Proof. intros H. by inversion H. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun