proposition: Lemma church_commute X (s: exp X) n: s = enc n -> lambda lambda (var 0) ((ren (shift >> shift) s) (var 1) (var 0)) ≡ lambda lambda (ren (shift >> shift) s) ((var 0) (var 1)) (var 0).
proof: Proof. intros ->. asimpl. change (var 0 (var 1)) with (AppL (repeat (@var X 0) 1) (var 1)). rewrite !enc_app, <-AppL_app, <-repeated_plus; now simplify. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)