等価性を持つメタ汎用の仮説を簡略化

Question

短い例を考え出すことができないのは残念です。

Iは

1. ⋀e1 T1 L e2 T2 G1. 
     typing (G1 @ (x, U) # G2) e1 T1 ⟹ 
     typing (G1 @ G2) e1 T1 ⟹ 
     (⋀xa. xa |∉| L ⟹ 
       typing ((xa, T1) # G1 @ (x, U) # G2) (open e2 (exp_fvar xa)) 
       T2) ⟹ 
     (⋀xa G1a. 
      xa |∉| L ⟹ 
      (xa, T1) # G1 = G1a ⟹ 
      x |∉| fv (open e2 (exp_fvar xa)) ⟹ 
      typing (G1a @ G2) (open e2 (exp_fvar xa)) T2) ⟹ 
     x |∉| fv e1 ⟹ x |∉| fv e2 ⟹ typing (G1 @ G2) (exp_let e1 e2) T2 

注意第前提（大きいもの）の証明状態を有する：それは普遍​​にわたってメタ定量化が、​​が実際にそこの式によって決定されます。だから、これを代用して（そして、前提の結論を簡素化することができ）、autoは目標を解決することができます。

シンプリファイアでこれを解決できますか？

私はequalities under existentialsについて多少関連する質問があり、小さな例が

lemma foo: 
    "(⋀ G. x#xs = G ⟹ P x ⟹ f G) ⟹ f (x#xs)" 
apply simp 

だと思います。

Answer 1

この問題は、simprocを使用してのみ確実に解決できます。すでにのinductプルーフメソッドが実装されているため、コードを変更することができます。考え方は、Induct.rearrange_eqs_simprocを使用して方程式を正面に移動し、適切な1点ルールを使用して等価を取り除くことです。