Set Implicit Arguments. Require Import CpdtTactics. Require Import List. Require Import JMeq. Check JMeq_eq. Check JMeq_ind_r. (*Check internal_JMeq_rew_r.*) Infix "==" := JMeq (at level 70, no associativity). Lemma pairC: forall A B1 B2 (x:A)(y1:B1)(y2:B2), y1==y2 -> (x,y1) == (x, y2). intros until y2. intro Hy. rewrite Hy. reflexivity. Qed. Print pairC. Check internal_JMeq_rew_r. (*forall (A : Type) (x : A) (B : Type) (b : B) (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x *) Lemma pairC': forall A B1 (x:A)(y1 y2:B1), y1==y2 -> (x,y1) == (x, y2). intros. apply pairC. assumption. Restart. intros. eapply internal_JMeq_rew_r with (2:=H). reflexivity. Restart. intros until y2. intro Hy. rewrite Hy. reflexivity. Qed. Print pairC'. Print Assumptions pairC'. Definition pairC'': forall A B1 (x:A)(y1 y2:B1), y1==y2 -> (x,y1) == (x, y2) := fun (A B1: Type) (x : A) (y1 y2: B1) (Hy : y1 == y2) => internal_JMeq_rew_r (fun (B3 : Type) (y3 : B3) => (x, y3) == (x, y2)) JMeq_refl Hy. Section fhlist. Variable A : Type. Variable B : A -> Type. Fixpoint fhlist (ls : list A) : Type := match ls with | nil => unit | x :: ls' => B x * fhlist ls' end%type. End fhlist. Section fhapp. Variable A : Type. Variable B : A -> Type. Fixpoint fhapp (ls1 ls2 : list A) : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) := match ls1 with | nil => fun _ hls2 => hls2 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) end. Implicit Arguments fhapp [ls1 ls2]. Theorem fhapp_assoc' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3. induction ls1; crush. rewrite IHls1. reflexivity. Restart. induction ls1; crush. generalize (fhapp b (fhapp hls2 hls3)) (fhapp (fhapp b hls2) hls3) (IHls1 _ _ b hls2 hls3). rewrite app_assoc. intros f f0 H. rewrite H. reflexivity. Qed. Print fhapp_assoc'. End fhapp. Print Assumptions fhapp_assoc'.