{P : Type} (a : P) (Q : forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac), Type) (s : Q a a idpath idpath idpath idpath) : forall b c ab ac bc abc, Q b c ab ac bc abc. Proof. intros. induction ab. induction bc. induction abc. apply s. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.